
;;;
;;; Solution for A3 question #5
;;;
;;; By Philip W. L. Fong
;;;

(defun prove (gamma alpha strategy)
  "Prove that wff ALPHA follows from wff GAMMA using search strategy STRATEGY."
  (let ((L-gamma (preprocess gamma))
	(L-alpha (preprocess (make-negation alpha))))
    (refute (append L-alpha L-gamma) strategy)))

